-- Created on: 2011-3-28
-- By: hujingfei914@msn.com

-- Module Definition
module Unify where

-- Type Definition
type ConstantType = String
type VariableType = String
type FunctionSymbol = String

data Term = Constant ConstantType | Variable VariableType | Function FunctionSymbol [Term]
	deriving Show
data Substitution = Substitute VariableType Term
	deriving Show


-- Function Definition: isBelong
-- Return true if a variable belongs to a term, or return false
-- Require: The format of the term resembles f(t) with f being function symbol and t being terms
isBelong :: VariableType -> Term -> Bool
isBelong variable (Function f ((Variable v) : terms)) = 
	if variable == v then
		True
	else
		isBelong variable (Function f terms)
isBelong variable (Function f ((Constant c) : terms)) =
	isBelong variable (Function f terms)
isBelong variable (Function f ((Function g embeddedTerms) : terms)) =
	if isBelong variable (Function g embeddedTerms) then 
		True 
	else 
		isBelong variable (Function f terms)
isBelong _ _ = False

-- Function Definition: assembleSubstitutions
-- Assemble two substitutions, return the compositive substitutions if feasible
assembleSubstitutions :: (Bool, [Substitution]) -> (Bool, [Substitution]) -> (Bool, [Substitution])
assembleSubstitutions (b1, sub1) (b2, sub2) =
	if b1 && b2 then
		(True, sub1 ++ sub2)
	else
		(False, [])

-- Function Definition: doSubstitute
-- Apply the substitution to the term, and return the resulted term
doSubstitute :: [Substitution] -> Term -> Term
doSubstitute [] term = term
doSubstitute [_] (Constant c) = Constant c
doSubstitute ((Substitute v1 t) : sub) (Variable v2) =
	if v1 == v2 then
		t
	else
		doSubstitute sub (Variable v2)
doSubstitute subs (Function f t) = 
	Function f (map (doSubstitute subs) t)


-- Function Definition: myunify
-- Return true and the corresponding substitution if the two input terms, t1 and t2, can be unified.
-- Or return false with a empty substitution set
myunify :: Term -> Term -> (Bool, [Substitution])
myunify (Constant t1) (Constant t2) =
	if t1 == t2 then 
		(True, []) 
	else 
		(False, [])
myunify (Variable t1) (Variable t2) =
	if t1 == t2 then 
		(True, [])
	else 
		(True, [Substitute t1 (Variable t2)])
-- if t1 is variable and t1 don't belong to t2, return True and the substitution t1 |-> t2
myunify (Variable t1) t2 = 
	if isBelong t1 t2 then 
		(False, []) 
	else
		(True, [Substitute t1 t2])
-- if t2 is variable and t2 don't belong to t1, return True and the substitution t2 |-> t1
myunify t1 (Variable t2) =
	if isBelong t2 t1 then
		(False, [])
	else
		(True, [Substitute t2 t1])
-- if t1 and t2 have the same outer function symbol, then 
myunify (Function f1 t1) (Function f2 t2) = 
	if (f1 /= f2 || length t1 /= length t2) then
		(False, [])
	else	-- Lambda function
		foldl (\ (bool, subs) (t1, t2) -> assembleSubstitutions (bool, subs) (myunify (doSubstitute subs t1) (doSubstitute subs t2))) 
		(True, []) (zip t1 t2)
myunify _ _ = (False, [])


-- Print help information
help = do
	putStrLn "Usage: myunify t1 t2"
	putStrLn "\tt1 and t2 are terms which could be such forms:"
	putStrLn "\t(Variable \"x\"), (Constant \"c\"), (Function \"f\" [t])"
	putStrLn "\t x, c and f could be any string and t is also term recursively"
	